/** Add css rules here for your application. */

h1 {
  font-size: 2em;
  font-weight: bold;
  margin: 1em 0px .2em;
  text-align: center;
}

h2 {
  font-size: 1.5em;
  font-weight: bold;
  margin: .4em 0px 1em;
}

h2, h3 {
  margin-bottom: .5em;
}

h4 {
  display: run-in;
}

h4:after {
  content: '. ';
}

body {
  margin: 1em 3em 1em 1em;
  text-align: left;
  font-family: sans-serif;
}

p {
  margin: 1em 0px;
  /*
   * Allow extra space for math formatting such as subscripts.
   * The plain number is inherited as-is, where a percentage or
   * em value, etc. is inherited as computed in the parent.
   */
  line-height: 1.4;
}

.italic {
  font-style: italic;
}

/* Makes an element display like a hyperlink. */
.link {
  color: #55F;
  cursor: pointer;
}

sub, sup {
  /* Prevents these from making the overall line less tall. */
  line-height: 0px;
  /* Browsers tend to size these for fractions, which makes */
  /* them a bit bigger than this. */
  font-size: 70%;
}

table {
  border-collapse: separate;
  empty-cells: show;
}

/* Source code (tty) style */
code {
  color: #860;
  white-space: nowrap;
  font-size: 110%;
}

/* Text wrapping */
.nowrap {
  white-space: nowrap;
}

.wrap {
  white-space: wrap;
}

/* Math-oriented text */
.math, .mathColor, s {
  font-family: STIXGeneral, Times, serif;
  /* Variable and constant names should be explicitly italicized
     within math text. */
  font-style: normal;
  white-space: nowrap;
}

/* Math text in documents */
.mathColor, s {
  color: #860;
}

.ellipsis {
  color: #888;
}

/* For rule menu descriptions */
.description {
  font-style: italic;
  color: gray;
}

/**
 * Truth tables for binary operators
 */

table.binaryTruthTable {
  border-collapse: collapse;
  margin-bottom: 1.5em;
}

table.binaryTruthTable td.truthy, table.binaryTruthTable td.falsy {
  padding: 2px 10px;
  border: 2px solid silver;
}

/* This needs to be less specific than a rule for class cellHighlight. */
td.falsy {
}

table.binaryTruthTable th {
  font-weight: normal;
  text-align: center;
  padding: 2px 10px;
}

/* This needs to take precedency over backgrounds for "falsy" cells. */
table.binaryTruthTable td.cellHighlight, .cellHighlight {
  background-color: #fcc;
}

.thHighlight {
  background-color: #fcc;
}

table.binaryTruthTable td.truthy:after {
  content: "true";
}

table.binaryTruthTable td.falsy:after {
  content: "false";
}


/* Just below the main heading */
div#slogans {
  color: ForestGreen;
  margin-bottom: 1em;
  text-align: center;
  font-style: italic;
}

/*
 * About the layout of Prooftoys pages and the use of SPAN tags
 *
 * Prooftoys is now using inline-block layout rather than the earlier
 * table-based layout.  IE7 and earlier only support the inline-block
 * style on tags with native inline layout, so #leftNav and #content
 * are SPAN tags.
 *
 * Table-based layout caused problems with unwanted early text
 * wrapping of deeply nested and indented expressions, so it had to
 * go.  Also, the current approach allows content to overflow the end
 * of line, which turns out to be a pretty good tradeoff over
 * everything trying to squeeze itself into the table width.
 */

/* Contains the left navigation */
span#leftNav {
  vertical-align: top;
  padding-top: 7em;
  display: inline-block;
  width: 20%;
  text-indent: -1em;
}

#leftNav a {
  display: block;
  font-style: italic;
  font-weight: bold;
  color: Indigo;
  text-decoration: none;
  margin: .3em 1em .3em 1em;
}

/* Left nav items */
#leftNav a:before {
  content: "⊦ ";
}

/* Entire main content of the page goes here */
#content {
  display: inline-block;
  width: 79%;
}

/* Text in a shaded box */
.explanation {
  margin: .3em;
  border: 4px solid silver; /* #ccf; */
  padding: 0em 1em;
  background-color: #e8e8ff;
}

/* Text in an unshaded box */
.boxed {
  margin: .3em;
  border: 4px solid silver;
  padding: .2em 1em;
}

/* Not displayed */
.hidden {
  display: none;
}

/* Invisibly fills space */
.invisible {
  visibility: hidden;
}

/* Proof displays -- proof.js */

/* Header line and comments for display. */
.proofHeader {
  margin: 0em 0em .4em .5em;
  padding-top: .2em;
  line-height: 120%;
}

/* Indent most subproofs. */
.proofDisplay .inferenceDisplay {
  margin: 5px 5px 5px 5px;
  border: 1px solid silver;
  box-shadow: 2px 2px 2px #ddd;
}

/* When inside an inferenceDisplay include a bit of bottom border.
   (The inferenceDisplay has its own border.)
 */
.proofDisplay .inferenceDisplay .proofDisplay {
  border-bottom: 3px solid transparent;
}

/* The first level of subproof needs extra indent in the case
 * where there is a "deleter" button on the left.
 */
.proofDisplay.editable .inferenceDisplay {
  margin-left: 3em;
}

.stepsParent {
  /* Can support absolute positioning of children; currently unused. */
  position: relative;
}

/*
 * Container for all the proof steps.  Slightly darker background
 * than the individual steps.
 */
.proofSteps {
  /* Touch screen tap highlighting is confusing, so prevent it. */
  -webkit-tap-highlight-color: rgba(0,0,0,0);
  /* For some reason the selection box shadow needs this margin. */
  margin: 5px 0px 1em;
  /* white-space: nowrap could go here to turn off text wrapping. */
}

.inferenceDisplay .proofSteps {
  margin-bottom: 0px;
}

/* The outermost element of a step */
.proofStep {
    background-color: white;
    font-family: STIXGeneral, times, serif;
    /* Each proofStep has a 1px border, which is gray when
       the step is selected in the UI or hovered.
       */
    border: 1px solid transparent;
    /* Indent continuation lines, but not the first one. */
    margin-left: 2em;
    /* Careful, this will be inherited by children. */
    text-indent: -2em;
}

/* Use the inline-block *class* as needed to avoid contaminating inner
   inline-block elements with the text-indent above. */
.proofStep .inline-block {
  display: inline-block;
  text-indent: 0em;
}

/* Subproof controls */

/*
 * Upward-pointing triangles that indicate a subproof is available.
 * Visible when step is hovered.
 */
.subproofIndicator {
  visibility: hidden;
}

.proofStep.hover .subproofIndicator {
  visibility: visible;
}

/* Display of element that can hide a subproof */
.subproofHider {
  visibility: hidden;
  font-family: sans-serif;
  font-style: italic;
  color: blue;
  cursor: pointer;
  background-color: #ddf;
  padding: 0px 6px;
  border: 1px solid #aaf;
}

/* If in a step with open subproof display or in a subproof, show it. */
.proofStep.hasSubproof .subproofHider, .proofHeader .subproofHider {
  visibility: visible;
}

/* Adjacent and similar to subproofHider */
.techDetailsButton {
  position: relative;
  font-family: sans-serif;
  font-style: italic;
  color: blue;
  cursor: pointer;
  background-color: #ddf;
  padding: 0px 6px;
  border: 1px solid #aaf;
}

.techDetails {
  margin: 0em .5em;
  padding: 2px 5px;
  border: 1px solid #bbb;
  background-color: aliceblue;
}

/* Statistics displays */

/* Time and step count statistics for proof or step. */
.ruleStats {
  margin-left: 2em;
  font-size: smaller;
  font-style: italic;
  color: gray;
}

/* Pop-up DIV that says Prooftoys is busy working. */
.ruleWorking {
  position: absolute;
  /* Initially hidden, will change over time and be given position. */
  display: none;
  z-index: 1;
  font-size: large;
  font-style: italic;
  color: red;
  background-color: #ffa;
  padding: .15em 2em;
  border: .2em solid #d00;
  box-shadow: 4px 4px 4px #888;
}

/* Hovering or selecting this will override the border color. */
.stepAndNum {
  cursor: default;
  border: 1px solid transparent;
}

/* Hovering the step number highlights the step and number,
 * indicating that the entire step can be selected.
 */
.proofDisplay.editable .proofStep .stepAndNum.hover {
  border-color: #88f;
}

/* But no hover in a subproof display */
.proofDisplay.editable .inferenceDisplay .stepAndNum.hover {
  border-color: transparent;
}

/* Step deleter control, only visible when the step is hovered. */
.proofStep .deleteStep {
  font-weight: bold;
  padding: .2em .4em;
  visibility: hidden;
}

/* Checkbox that selects an entire step.  Visible when the
   step is hovered or selected. */
.proofStep .checkbox {
  visibility: hidden;
}

.proofStep.hover .deleteStep {
  visibility: visible;
  color: red;
}

.proofStep.hover .checkbox, .proofStep.selected .checkbox {
  visibility: visible;
}

/* The noDeleter contains an indicator that the step is hovered. */
.proofStep .noDeleter {
  visibility: hidden;
}

.proofStep.hover .noDeleter {
  color: #aaa;
  visibility: visible;
} 

/* The step has other steps that depend on it. */
.proofStep.hover.hasUsers .deleteStep {
  visibility: visible;
  color: silver;
}

/* Rule name and information about rule arguments. */
.proofStep .stepInfo {
    white-space: nowrap;
    color: #777;
}

.proofStep .stepNumber {
  /* Like stepInfo */
  color: #777;
}


/* Highlighting of parts of proof steps */

.proofStep.dep .stepNumArea {
  background-color: #af6;
 }

/* The "site" class requests display of the expr as a
   "site" input of a proof step.
 */
.proofStep .expr.site {
  background-color: #af6;
}

/* Must be specific enough to override the silver/gray border. */
.proofDisplay.editable .proofStep.selected .stepAndNum {
  border: 1px solid #888;
  box-shadow: 2px 2px 2px #888;
}

/* Old value ("removed"), occurrence of variable to be substituted. */
.proofStep .old, .proofStep .occur {
  color: #A0A0A0; /* Between silver and gray */
}

/* Scope of operation, e.g. function body to substitute into.
 * Lower priority than "new", so precedes it in the file.
 */
.proofStep .scope {
  background-color: #eee;
}

/* New value ("replacement") -- green */
.proofStep .new {
  background-color: #af6;
}

/* References to a step number, where it is used as an input */
span.stepReference.referenced {
  border-color: #88F;
}

/* Rule name (or fact used for rewriting) */
span.ruleName {
  font-style: italic;
}

/* To prevent clicks in rapid succession from highlighting text
   or activating a double click action. */
span.ruleName.link, .stepAndNum, 

/* This class prevents the user from selecting text. */
.noselect {
  /* Including browser-specific versions */
  -webkit-touch-callout: none;
  -webkit-user-select: none;
  -khtml-user-select: none;
  -moz-user-select: moz-none;
  -ms-user-select: none;
  user-select: none;
}

.expr {
  position: relative;
}

/* Expression in a proof step display, and step numbers */
.proofStep .expr, span.stepNumber, span.stepReference {
  border-style: solid;
  border-width: 1px;
  border-color: transparent;
}

span.assumptions {
  color: #999;
  margin-left: .3em;
  margin-right: .1em;
}

/* Step reference in assumptions */
span.stepRef {
  font-weight: bold;
}

/* Holder for information shown "above" an expression. */
.above {
  position: absolute;
  visibility: hidden;
  cursor: pointer;
  left: -1px;
  bottom: 1.5em;
  min-width: 100%;
  padding: 2px 2px;
  border: 1px solid gray;
  white-space: nowrap;
  background-color: lightyellow;
  /* Overrides .proofStep: */
  text-indent: 0em;
  box-shadow: 2px 2px 2px #aaa;
}

.above.hover {
  opacity: 1;
}

/* The element is visible when its expression is hovered. */
.fullExpr.popped > .above {
  visibility: visible;
}

/* When hovering over an expression in an editable proof.
   See also .stepAndNum .hover.
 */
.expr.hover {
  border-color: #88f;
}

/* Highlight selected expressions; a bit over-specific
   to take precedence over the hover highlight. */
.proofDisplay.editable .proofStep .expr.selected {
  border-color: DarkGray;
  box-shadow: 2px 2px 2px #aaa;
}

/* Styling for constants T and F, sans-serif roman. */
.proofStep .expr .trueFalse {
  font-family: sans-serif;
  font-size: 90%;
}


/* Proof step editor */

.proofErrors {
  padding: 4px;
  border: 2px solid DarkSeaGreen;
  border-radius: 5px;
  margin: 1em 0em;
}

/* Overrides styles for .proofDisplay. */
.stepEditor {
  background-color: white;
  margin-top: .2em;
  position: relative;
}

/* Make inputs a bit larger than regular text */
.stepEditor input {
  font-family: STIXGeneral, times;
  font-size: 90%;
}

.stepEditor select {
  font-size: 120%;
}

.rules-header {
  padding-left: 4px;
  font-weight: bold;
}

.stepEditor .ruleSelector {
  min-height: 20em;
}

/* Text used as a hint, as in a text field */
.hinted {
  font-style: italic;
  font-size: 90%;
  color: #999;
}

/* Input for rule name */
input.sted-input {
  font-family: inherit;
  font-size: 100%;
  width: 80%;
}

/* Button to clear the current editor input form */
input.sted-clear {
  /* Lines it up better with the adjacent text */
  vertical-align: text-bottom;
}

/* Inputs for rule arguments */

/* input.string is currently just used for defined names */
input.term, input.string {
  font-style: italic;
  width: 30em;
}

input.varName, input.step, input.equation, input.implication {
  width: 4em;
}

/* Rule selection items */

.ruleItem:hover {
  left: -1px;
  top: -1px;
  border: 1px solid #aaa;
  box-shadow: 1px 1px 1px #aaa;
  background-color: #fbfbf9;
}

.ruleItem, .ruleItem:active {
  position: relative;
  left: 0px;
  top: 0px;
  margin: 2px 1px;
  padding: 2px 4px;
  border: 1px solid #eee;
  border-radius: 4px;
  cursor: pointer;
  box-shadow: none;
}

.ruleItem:active {
  background-color: #aaf;
  border-color: gray;
}

/* Proof state display */

.proofStateDisplay {
    padding: 1em;
    border: 2px solid #aaf;
}

textarea.proofStateArea {
    width: 95%;
    margin: 1em 0em;
}
